
\modifica{m}
\asegura{mismos(secretarias(m), secretarias(pre(m)))}
\asegura{(\forall pcia \selec secretarias(m))(\forall hotel \selec registro(m, pcia)) \\
	cadena(hotel) == cadena(dameHotelDeProvincia(pre(m), pcia, nombre(hotel))) \wedge \\
	mismos(huespedes(hotel), huespedes(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	mismos(ingresos(hotel), ingresos(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	mismos(salidas(hotel), salidas(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	mismos(reservas(hotel), reservas(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	mismos(tarifaHabitacionXDia(hotel), tarifaHabitacionXDia(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	mismos(precioAccesorio(hotel), precioAccesorio(dameHotelDeProvincia(pre(m), pcia, nombre(hotel)))) \wedge \\
	(\forall habitacion \selec habitaciones(hotel))( \\
	tipo(habitacion) == dameHabitacion(pre(m), pcia, nombre(hotel), numero(habitacion)) \wedge \\
	mismos(accesorios(habitacion), \\
	\comp{acc}{acc \selec accesorios(dameHabitacion(pre(m), pcia, nombre(hotel), numero(habitacion))), (acc \neq LCD)}))}

\asegura{(\forall cadena \selec cadenasDeHoteles(m))(\forall hotel \selec cadena) \\
	mismos(huespedes(hotel), huespedes(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	mismos(ingresos(hotel), ingresos(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	mismos(salidas(hotel), salidas(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	mismos(reservas(hotel), reservas(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	mismos(tarifaHabitacionXDia(hotel), tarifaHabitacionXDia(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	mismos(precioAccesorio(hotel), precioAccesorio(dameHotelDeCadena(pre(m), nombre(hotel), cadena))) \wedge \\
	(\forall habitacion \selec habitaciones(hotel))( \\
	tipo(habitacion) == dameHabitacionDeCadena(pre(m), nombre(hotel), cadena(hotel), numero(habitacion)) \wedge \\
	mismos(accesorios(habitacion), \\
	\comp{acc}{acc \selec accesorios(dameHabitacionDeCadena(pre(m), nombre(hotel), cadena(hotel), numero(habitacion))), (acc \neq LCD)}))}

\asegura{result == LCDs(pre(m))}

\aux{dameHotelDeProvincia}{m: MinisterioDeTurismo, p: Provincia, n: Nombre}{Hotel}{\\
	\comp{h}{h \selec registro(m, p), nombre(h) == n}[0]}
\aux{dameHabitacion}{m: MinisterioDeTurismo, p: Provincia, n: Nombre, numero: \ent}{Habitacion}{\\
	\comp{hab}{hotel \selec registro(m, p), hab \selec habitaciones(hotel), nombre(hotel) == n \wedge numero(hab) == numero}[0]}
\aux{dameHotelDeCadena}{m: MinisterioDeTurismo, nombre: Nombre, cadena: Cadena}{Hotel}{\\
	\comp{hotel}{hoteles \selec cadenasDeHoteles(m), hotel \selec hoteles, nombre(hotel) == nombre \wedge cadena(hotel) == cadena}[0]}
\aux{dameHabitacionDeCadena}{m: MinisterioDeTurismo, nombre: Nombre, cadena: Cadena, numero: \ent}{Habitacion}{\\
	\comp{habitacion}{habitacion \selec habitaciones(dameHotelDeCadena(m, nombre, cadena)), numero(habitacion) == numero}[0]}

\aux{LCDs}{m: MinisterioDeTurismo}{\ent}{sum(\comp{\IfThenElse{en(LCD, accesorios(habitacion))}{1}{0}}{ \\
	hoteles \selec cadenasDeHoteles(m), \\
	hotel \selec hoteles, \\
	habitacion \selec habitaciones(hotel)})}
